Inference at * 1 1 2 0 
Iof proof for Lemma l before antisymmetry:



1. T : Type
2. l : T List
3. x : T
4. y : T
5. no_repeats(T;l)
6. [x; y]  l
7. [y; x]  l
  [x; y; x]  l 

latex

 by PERMUTE{1:n, 2:n, 2:n, 3:n, 4:n, 5:n, 6:n, 7:n, 8:n} 

latex

 1: .....wf..... NILNIL

 1:   T  Type
 2: .....wf..... NILNIL

 2:   [x]  (T List)
 3: .....wf..... NILNIL

 3:   l  (T List)
 4: .....wf..... NILNIL

 4:   y  T
 5: .....antecedent..... NILNIL

 5:   no_repeats(T;l)
 6: 

 6:   [x] @ [y]  l
 7: .....antecedent..... NILNIL

 7:   [y; x]  l
 8: 

 8: 8. [x] @ [y; x]  l
 8:   [x; y; x]  l
 .

Definitions	t  T, f(a), s = t, x:AB(x), as @ bs, [], [car / cdr], L1  L2, no_repeats(T;l), type List, Type, P  Q, x:A. B(x)
Lemmas	append overlapping sublists